package systemf;

import java.util.ArrayList;
import java.util.List;

/**
 * System F解析器
 * 解析文本表示到Term和Type对象
 */
public class Parser {
    
    private String input;
    private int pos;
    
    public Parser(String input) {
        this.input = input.trim();
        this.pos = 0;
    }
    
    /**
     * 解析项
     */
    public Term parseTerm() {
        skipWhitespace();
        
        // Lambda抽象: λx:τ.M 或 Λα.M
        if (peek() == 'λ') {
            return parseLambda();
        } else if (peek() == 'Λ') {
            return parseTypeAbs();
        }
        
        // 应用或类型应用
        Term term = parseAtom();
        
        while (true) {
            skipWhitespace();
            if (pos >= input.length()) break;
            
            char c = peek();
            if (c == '[') {
                // 类型应用 M[τ]
                term = parseTypeApp(term);
            } else if (c == '(' || Character.isLetter(c) || c == 'λ' || c == 'Λ') {
                // 应用 M N
                Term arg = parseAtom();
                term = new Term.App(term, arg);
            } else {
                break;
            }
        }
        
        return term;
    }
    
    /**
     * 解析原子项（变量或括号表达式）
     */
    private Term parseAtom() {
        skipWhitespace();
        
        if (peek() == '(') {
            // 括号表达式
            expect('(');
            Term term = parseTerm();
            expect(')');
            return term;
        } else if (Character.isLetter(peek())) {
            // 变量
            String name = parseIdentifier();
            return new Term.Var(name);
        } else if (peek() == 'λ') {
            return parseLambda();
        } else if (peek() == 'Λ') {
            return parseTypeAbs();
        }
        
        throw new ParseException("意外的字符: " + peek() + " 在位置 " + pos);
    }
    
    /**
     * 解析Lambda抽象: λx:τ.M
     */
    private Term parseLambda() {
        expect('λ');
        String var = parseIdentifier();
        expect(':');
        Type type = parseType();
        expect('.');
        Term body = parseTerm();
        return new Term.Lambda(var, type, body);
    }
    
    /**
     * 解析类型抽象: Λα.M
     */
    private Term parseTypeAbs() {
        expect('Λ');
        String typeVar = parseIdentifier();
        expect('.');
        Term body = parseTerm();
        return new Term.TypeAbs(typeVar, body);
    }
    
    /**
     * 解析类型应用: M[τ]
     */
    private Term parseTypeApp(Term term) {
        expect('[');
        Type type = parseType();
        expect(']');
        return new Term.TypeApp(term, type);
    }
    
    /**
     * 解析类型
     */
    public Type parseType() {
        skipWhitespace();
        
        // 全称类型: ∀α.τ
        if (peek() == '∀') {
            return parseForallType();
        }
        
        // 函数类型或基本类型
        Type left = parseAtomType();
        
        skipWhitespace();
        if (pos < input.length() && peek() == '→') {
            expect('→');
            Type right = parseType();
            return new Type.ArrowType(left, right);
        }
        
        return left;
    }
    
    /**
     * 解析原子类型（基本类型、类型变量或括号类型）
     */
    private Type parseAtomType() {
        skipWhitespace();
        
        if (peek() == '(') {
            expect('(');
            Type type = parseType();
            expect(')');
            return type;
        } else if (Character.isLetter(peek())) {
            String name = parseIdentifier();
            // 简单判断：小写字母开头的可能是类型变量，大写或特定名称是基本类型
            if (name.length() == 1 && Character.isLowerCase(name.charAt(0))) {
                return new Type.TypeVar(name);
            }
            return new Type.BaseType(name);
        } else if (peek() == '∀') {
            return parseForallType();
        }
        
        throw new ParseException("意外的类型字符: " + peek() + " 在位置 " + pos);
    }
    
    /**
     * 解析全称类型: ∀α.τ
     */
    private Type parseForallType() {
        expect('∀');
        String typeVar = parseIdentifier();
        expect('.');
        Type body = parseType();
        return new Type.ForallType(typeVar, body);
    }
    
    /**
     * 解析标识符
     */
    private String parseIdentifier() {
        skipWhitespace();
        if (pos >= input.length() || !Character.isLetter(input.charAt(pos))) {
            throw new ParseException("期望标识符，得到: " + (pos < input.length() ? peek() : "EOF"));
        }
        
        StringBuilder sb = new StringBuilder();
        while (pos < input.length() && 
               (Character.isLetterOrDigit(input.charAt(pos)) || input.charAt(pos) == '_')) {
            sb.append(input.charAt(pos++));
        }
        return sb.toString();
    }
    
    /**
     * 跳过空白字符
     */
    private void skipWhitespace() {
        while (pos < input.length() && Character.isWhitespace(input.charAt(pos))) {
            pos++;
        }
    }
    
    /**
     * 查看当前字符（不移动位置）
     */
    private char peek() {
        if (pos >= input.length()) return '\0';
        return input.charAt(pos);
    }
    
    /**
     * 期望特定字符
     */
    private void expect(char c) {
        skipWhitespace();
        if (pos >= input.length() || input.charAt(pos) != c) {
            throw new ParseException("期望 '" + c + "', 得到: " + 
                                   (pos < input.length() ? input.charAt(pos) : "EOF") +
                                   " 在位置 " + pos);
        }
        pos++;
    }
    
    /**
     * 解析异常
     */
    public static class ParseException extends RuntimeException {
        public ParseException(String message) {
            super(message);
        }
    }
}

